(set-logic QF_LIA)
(set-info :source |
Alberto Griggio

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun z3_31_0_ () Int)
(declare-fun z3_7_0_ () Int)
(declare-fun z3_31_8_ () Int)
(declare-fun z11_31_0_ () Int)
(declare-fun z11_0_0_ () Int)
(declare-fun z11_31_1_ () Int)
(declare-fun z22_30_0_ () Int)
(declare-fun z24_30_0_ () Int)
(declare-fun sigma_26_ () Int)
(declare-fun z27_30_0_ () Int)
(declare-fun sigma_29_ () Int)
(declare-fun sigma_31_ () Int)
(declare-fun sigma_35_ () Int)
(declare-fun z39_31_0_ () Int)
(declare-fun z42_23_0_ () Int)
(declare-fun z46_31_0_ () Int)
(declare-fun z46_7_0_ () Int)
(declare-fun z46_31_8_ () Int)
(declare-fun z50_31_0_ () Int)
(declare-fun z50_0_0_ () Int)
(declare-fun z50_31_1_ () Int)
(declare-fun z61_31_0_ () Int)
(declare-fun z63_23_0_ () Int)
(declare-fun z67_31_0_ () Int)
(declare-fun z69_23_0_ () Int)
(declare-fun z74_31_0_ () Int)
(declare-fun z76_23_0_ () Int)
(declare-fun z79_31_0_ () Int)
(declare-fun z86_31_0_ () Int)
(declare-fun z86_7_0_ () Int)
(declare-fun z86_31_8_ () Int)
(declare-fun z88_31_0_ () Int)
(declare-fun z88_7_0_ () Int)
(declare-fun z88_31_8_ () Int)
(declare-fun z91_31_0_ () Int)
(declare-fun z91_7_0_ () Int)
(declare-fun z91_31_8_ () Int)
(declare-fun z93_31_0_ () Int)
(declare-fun z93_7_0_ () Int)
(declare-fun z93_31_8_ () Int)
(declare-fun z96_31_0_ () Int)
(declare-fun z96_7_0_ () Int)
(declare-fun z96_31_8_ () Int)
(declare-fun z98_31_0_ () Int)
(declare-fun z98_7_0_ () Int)
(declare-fun z98_31_8_ () Int)
(declare-fun z101_31_0_ () Int)
(declare-fun z101_7_0_ () Int)
(declare-fun z101_31_8_ () Int)
(declare-fun z103_23_0_ () Int)
(declare-fun z103_7_0_ () Int)
(declare-fun z103_23_8_ () Int)
(declare-fun z98_23_0_ () Int)
(declare-fun z98_31_24_ () Int)
(declare-fun z24_23_0_ () Int)
(declare-fun z24_30_24_ () Int)
(declare-fun z93_23_0_ () Int)
(declare-fun z93_31_24_ () Int)
(declare-fun z22_23_0_ () Int)
(declare-fun z22_30_24_ () Int)
(declare-fun z88_23_0_ () Int)
(declare-fun z88_31_24_ () Int)
(declare-fun z27_23_0_ () Int)
(declare-fun z27_30_24_ () Int)
(declare-fun z121_31_0_ () Int)
(declare-fun z121_23_0_ () Int)
(declare-fun z121_31_24_ () Int)
(declare-fun z46_23_0_ () Int)
(declare-fun z46_31_24_ () Int)
(declare-fun z3_23_0_ () Int)
(declare-fun z3_31_24_ () Int)
(declare-fun z126_7_0_ () Int)
(declare-fun z127_30_0_ () Int)
(declare-fun z127_22_0_ () Int)
(declare-fun z127_30_23_ () Int)
(assert (let ((?v_0 (+ (+ z24_30_0_ z22_30_0_) z27_30_0_))) (let ((?v_1 (+ ?v_0 (* sigma_31_ (- 2147483648))))) (let ((?v_2 (not (<= 1073741823 ?v_1)))) (let ((?v_3 (and (not (<= ?v_1 (- 1))) ?v_2)) (?v_5 (not (and (not (<= ?v_1 0)) ?v_2))) (?v_4 (+ (* sigma_35_ (- 2147483648)) z24_30_0_))) (and (and (<= sigma_31_ 3) (<= 0 sigma_31_)) (and (and (<= sigma_29_ 2) (<= 0 sigma_29_)) (and (and (<= sigma_35_ 1) (<= 0 sigma_35_)) (and (and (<= sigma_26_ 1) (<= 0 sigma_26_)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= z127_30_23_ z126_7_0_) (= (+ (- z121_31_24_) (* z27_30_24_ 2)) 0)) (= (+ (* z27_30_24_ (- 2)) z88_31_24_) 0)) (= (+ (* z22_30_24_ (- 2)) z93_31_24_) 0)) (= (+ (* z24_30_24_ (- 2)) z98_31_24_) 0)) (= z103_7_0_ z101_7_0_)) (= z98_7_0_ z96_7_0_)) (= z93_7_0_ z91_7_0_)) (= z88_7_0_ z86_7_0_)) (not (= z24_30_0_ 0))) (not (and (not (<= z79_31_0_ 16)) (not (<= 2147483648 z79_31_0_))))) (or (= z76_23_0_ 0) (= z74_31_0_ 2))) (= (+ (* sigma_29_ (- 2147483648)) ?v_0) 0)) (and (not (<= ?v_1 (- 2))) ?v_2)) (or (= z69_23_0_ 0) (= z67_31_0_ 2))) ?v_3) (or (= z63_23_0_ 0) (= z61_31_0_ 2))) ?v_3) (ite (not (and (not (<= ?v_1 126)) ?v_2)) (= z50_31_0_ 1) (= z50_31_0_ 0))) (ite (not (= z50_0_0_ 1)) (= z46_7_0_ 1) (= z46_7_0_ 0))) ?v_5) (or (= z42_23_0_ 0) (= z39_31_0_ 2))) (not (and (not (<= ?v_4 126)) (not (<= 1073741823 ?v_4))))) (ite ?v_5 (= z11_31_0_ 1) (= z11_31_0_ 0))) (ite (not (= z11_0_0_ 1)) (= z3_7_0_ 1) (= z3_7_0_ 0))) (and (not (<= 4294967296 z3_31_0_)) (<= 0 z3_31_0_))) (and (not (<= 256 z3_7_0_)) (<= 0 z3_7_0_))) (and (not (<= 16777216 z3_31_8_)) (<= 0 z3_31_8_))) (= (+ (+ (- z3_7_0_) z3_31_0_) (* z3_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z11_31_0_)) (<= 0 z11_31_0_))) (and (not (<= 2 z11_0_0_)) (<= 0 z11_0_0_))) (and (not (<= 2147483648 z11_31_1_)) (<= 0 z11_31_1_))) (= (+ (+ (- z11_0_0_) z11_31_0_) (* z11_31_1_ (- 2))) 0)) (and (not (<= 2147483648 z22_30_0_)) (<= 0 z22_30_0_))) (and (not (<= 2147483648 z24_30_0_)) (<= 0 z24_30_0_))) (and (not (<= 2147483648 z27_30_0_)) (<= 0 z27_30_0_))) (and (not (<= 4294967296 z39_31_0_)) (<= 0 z39_31_0_))) (and (not (<= 16777216 z42_23_0_)) (<= 0 z42_23_0_))) (and (not (<= 4294967296 z46_31_0_)) (<= 0 z46_31_0_))) (and (not (<= 256 z46_7_0_)) (<= 0 z46_7_0_))) (and (not (<= 16777216 z46_31_8_)) (<= 0 z46_31_8_))) (= (+ (+ (- z46_7_0_) z46_31_0_) (* z46_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z50_31_0_)) (<= 0 z50_31_0_))) (and (not (<= 2 z50_0_0_)) (<= 0 z50_0_0_))) (and (not (<= 2147483648 z50_31_1_)) (<= 0 z50_31_1_))) (= (+ (+ (- z50_0_0_) z50_31_0_) (* z50_31_1_ (- 2))) 0)) (and (not (<= 4294967296 z61_31_0_)) (<= 0 z61_31_0_))) (and (not (<= 16777216 z63_23_0_)) (<= 0 z63_23_0_))) (and (not (<= 4294967296 z67_31_0_)) (<= 0 z67_31_0_))) (and (not (<= 16777216 z69_23_0_)) (<= 0 z69_23_0_))) (and (not (<= 4294967296 z74_31_0_)) (<= 0 z74_31_0_))) (and (not (<= 16777216 z76_23_0_)) (<= 0 z76_23_0_))) (and (not (<= 4294967296 z79_31_0_)) (<= 0 z79_31_0_))) (and (not (<= 4294967296 z86_31_0_)) (<= 0 z86_31_0_))) (and (not (<= 256 z86_7_0_)) (<= 0 z86_7_0_))) (and (not (<= 16777216 z86_31_8_)) (<= 0 z86_31_8_))) (= (+ (+ (- z86_7_0_) z86_31_0_) (* z86_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z88_31_0_)) (<= 0 z88_31_0_))) (and (not (<= 256 z88_7_0_)) (<= 0 z88_7_0_))) (and (not (<= 16777216 z88_31_8_)) (<= 0 z88_31_8_))) (= (+ (+ (- z88_7_0_) z88_31_0_) (* z88_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z91_31_0_)) (<= 0 z91_31_0_))) (and (not (<= 256 z91_7_0_)) (<= 0 z91_7_0_))) (and (not (<= 16777216 z91_31_8_)) (<= 0 z91_31_8_))) (= (+ (+ (- z91_7_0_) z91_31_0_) (* z91_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z93_31_0_)) (<= 0 z93_31_0_))) (and (not (<= 256 z93_7_0_)) (<= 0 z93_7_0_))) (and (not (<= 16777216 z93_31_8_)) (<= 0 z93_31_8_))) (= (+ (+ (- z93_7_0_) z93_31_0_) (* z93_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z96_31_0_)) (<= 0 z96_31_0_))) (and (not (<= 256 z96_7_0_)) (<= 0 z96_7_0_))) (and (not (<= 16777216 z96_31_8_)) (<= 0 z96_31_8_))) (= (+ (+ (- z96_7_0_) z96_31_0_) (* z96_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z98_31_0_)) (<= 0 z98_31_0_))) (and (not (<= 256 z98_7_0_)) (<= 0 z98_7_0_))) (and (not (<= 16777216 z98_31_8_)) (<= 0 z98_31_8_))) (= (+ (+ (- z98_7_0_) z98_31_0_) (* z98_31_8_ (- 256))) 0)) (and (not (<= 4294967296 z101_31_0_)) (<= 0 z101_31_0_))) (and (not (<= 256 z101_7_0_)) (<= 0 z101_7_0_))) (and (not (<= 16777216 z101_31_8_)) (<= 0 z101_31_8_))) (= (+ (+ (- z101_7_0_) z101_31_0_) (* z101_31_8_ (- 256))) 0)) (and (not (<= 16777216 z103_23_0_)) (<= 0 z103_23_0_))) (and (not (<= 256 z103_7_0_)) (<= 0 z103_7_0_))) (and (not (<= 65536 z103_23_8_)) (<= 0 z103_23_8_))) (= (+ (+ (- z103_7_0_) z103_23_0_) (* z103_23_8_ (- 256))) 0)) (and (not (<= 16777216 z98_23_0_)) (<= 0 z98_23_0_))) (and (not (<= 256 z98_31_24_)) (<= 0 z98_31_24_))) (= (+ (+ (- z98_23_0_) z98_31_0_) (* z98_31_24_ (- 16777216))) 0)) (and (not (<= 16777216 z24_23_0_)) (<= 0 z24_23_0_))) (and (not (<= 128 z24_30_24_)) (<= 0 z24_30_24_))) (= (+ (+ (- z24_23_0_) z24_30_0_) (* z24_30_24_ (- 16777216))) 0)) (and (not (<= 16777216 z93_23_0_)) (<= 0 z93_23_0_))) (and (not (<= 256 z93_31_24_)) (<= 0 z93_31_24_))) (= (+ (+ (- z93_23_0_) z93_31_0_) (* z93_31_24_ (- 16777216))) 0)) (and (not (<= 16777216 z22_23_0_)) (<= 0 z22_23_0_))) (and (not (<= 128 z22_30_24_)) (<= 0 z22_30_24_))) (= (+ (+ (- z22_23_0_) z22_30_0_) (* z22_30_24_ (- 16777216))) 0)) (and (not (<= 16777216 z88_23_0_)) (<= 0 z88_23_0_))) (and (not (<= 256 z88_31_24_)) (<= 0 z88_31_24_))) (= (+ (+ (- z88_23_0_) z88_31_0_) (* z88_31_24_ (- 16777216))) 0)) (and (not (<= 16777216 z27_23_0_)) (<= 0 z27_23_0_))) (and (not (<= 128 z27_30_24_)) (<= 0 z27_30_24_))) (= (+ (+ (- z27_23_0_) z27_30_0_) (* z27_30_24_ (- 16777216))) 0)) (and (not (<= 4294967296 z121_31_0_)) (<= 0 z121_31_0_))) (and (not (<= 16777216 z121_23_0_)) (<= 0 z121_23_0_))) (and (not (<= 256 z121_31_24_)) (<= 0 z121_31_24_))) (= (+ (+ (- z121_23_0_) z121_31_0_) (* z121_31_24_ (- 16777216))) 0)) (and (not (<= 16777216 z46_23_0_)) (<= 0 z46_23_0_))) (and (not (<= 256 z46_31_24_)) (<= 0 z46_31_24_))) (= (+ (+ (- z46_23_0_) z46_31_0_) (* z46_31_24_ (- 16777216))) 0)) (and (not (<= 16777216 z3_23_0_)) (<= 0 z3_23_0_))) (and (not (<= 256 z3_31_24_)) (<= 0 z3_31_24_))) (= (+ (+ (- z3_23_0_) z3_31_0_) (* z3_31_24_ (- 16777216))) 0)) (and (not (<= 256 z126_7_0_)) (<= 0 z126_7_0_))) (and (not (<= 2147483648 z127_30_0_)) (<= 0 z127_30_0_))) (and (not (<= 8388608 z127_22_0_)) (<= 0 z127_22_0_))) (and (not (<= 256 z127_30_23_)) (<= 0 z127_30_23_))) (= (+ (+ (- z127_22_0_) z127_30_0_) (* z127_30_23_ (- 8388608))) 0)))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
